|
In computer science and automata theory, a Büchi automaton is a type of ω-automaton, which extends a finite automaton to infinite inputs. It accepts an infinite input sequence if there exists a run of the automaton that visits (at least) one of the final states infinitely often. Büchi automata recognize the omega-regular languages, the infinite word version of regular languages. It is named after the Swiss mathematician Julius Richard Büchi who invented this kind of automaton in 1962. Büchi automata are often used in model checking as an automata-theoretic version of a formula in linear temporal logic. ==Formal definition== Formally, a deterministic Büchi automaton is a tuple ''A'' = (''Q'',Σ,δ,''q''0,F) that consists of the following components: * ''Q'' is a finite set. The elements of ''Q'' are called the ''states'' of ''A''. * Σ is a finite set called the ''alphabet'' of ''A''. * δ: ''Q'' × Σ → ''Q'' is a function, called the ''transition function'' of ''A''. * ''q''0 is an element of ''Q'', called the ''initial state'' of ''A''. * F⊆''Q'' is the ''acceptance condition''. ''A'' accepts exactly those runs in which at least one of the infinitely often occurring states is in F. In a non-deterministic Büchi automaton, the transition function δ is replaced with a transition relation Δ that returns a set of states, and the single initial state ''q''0 is replaced by a set ''I'' of initial states. Generally, the term Büchi automaton without qualifier refers to non-deterministic Büchi automata. For more comprehensive formalism see also ω-automaton. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Büchi automaton」の詳細全文を読む スポンサード リンク
|